#include <stdio.h>
#include <stdint.h>
#include <inttypes.h>
#include <vector>

#include <klee/klee.h>

using namespace std;

#if __WORDSIZE == 64
#define U64 "lu"
#else
#define U64 "llu"
#endif

uint64_t i;
vector<int> v;

int foo() {
	int i = 2;
	tern_symbolic(&i, sizeof(i), "i_switch");	
	switch (i) {
		case 0:
			fprintf(stderr, "i = 0\n");
			break;
		case 1:
			fprintf(stderr, "i = 1\n");
//			break;
		case 2:
			fprintf(stderr, "i = 2\n");
			break;
		default:
			fprintf(stderr, "i = ?\n");
			break;
	};	
	fprintf(stderr, "i = foo\n");
	return 1;
}

int main (int argc, char *argv[]) {
	return foo();
}
